\documentclass{article}

\usepackage{amssymb}

\begin{document}

{\addtolength{\parskip}{1em}

$X$ is the set of all variables. $x \in X$.

$E$ is the set of all expressions. $e \in E$.

$Z$ is the set of all integer values. $z \in Z$.

$\sigma$ is the store. $\sigma(x)$ retrieves a value from
the store. $\sigma \left[ x \leftarrow z \right]$ is the
store $\sigma$, but where the value of $x$ is $z$.

$P$ is the program. It acts as a function of line numbers,
returning the statement at the given number. For example,
$P(2)$ represents the statement at line 2. When given the
line number just beyond the last statement in the program,
$P$ returns the special symbol $end$.

$\frac
{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{:} \, x \, \mathrm{=} \, e, \, \sigma \right>
\rightarrow
\left< l \mathrm{:} \, x \, \mathrm{=} \, e', \, \sigma' \right>}
$

$\frac
{x \in Dom(\sigma)}
{\left< l \mathrm{:} \, x \, \mathrm{=} \, z, \, \sigma \right>
\rightarrow
\left< P(l+1), \,  \sigma \left[ x \leftarrow z \right] \right>}$

$\frac
{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \, \mathrm{=} \, e, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \, \mathrm{=} \, e', \, \sigma' \right>}
$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} e \mathrm{]}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} e' \mathrm{]}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} e \mathrm{] \, = \{}
e_1, \, \dots \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} e' \mathrm{] \, = \{}
e_1, \, \dots \mathrm{\}}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma) \; \;
\left< e_1, \, \sigma \right> \rightarrow \left< e_1', \, \sigma' \right>}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, e_1, \, \dots \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, e_1', \, \dots \mathrm{\}}, \, \sigma' \right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{] \, = \{}
z_1, \, \dots, \, z_z \mathrm{\}}, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma
\left[x \leftarrow undef \right]
\left[len(x) \leftarrow z \right]
\left[x[0] \leftarrow z_1 \right]
\left[x[1] \leftarrow z_2 \right]
\dots
\left[x[z-1] \leftarrow z_z \right]
\right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l \mathrm{: \, int} \; x \mathrm{[} z \mathrm{]}, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma
\left[x \leftarrow undef \right]
\left[len(x) \leftarrow z \right]
\left[x[0] \leftarrow undef \right]
\left[x[1] \leftarrow undef \right]
\dots
\left[x[z-1] \leftarrow undef \right]
\right>}$

$\frac
{x \notin Dom(\sigma)}
{\left< l\mathrm{: \, int} \; x \, \mathrm{=} \, z, \, \sigma \right>
\rightarrow
\left< P(l+1), \,  \sigma \left[ x \leftarrow z \right] \right>}$

$\frac{x \notin Dom(\sigma)}
{\left< l\mathrm{: \, int} \; x, \, \sigma \right>
\rightarrow
\left< P(l+1), \, \sigma \left[ x \leftarrow undef \right] \right>}$

$\frac{}
{\left< l_1 \mathrm{: \, goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_2), \, \sigma \right>}$

$\frac{\left< e, \, \sigma \right> \rightarrow \left< e' \sigma' \right>}
{\left<  l_1 \mathrm{: \, if \; (} e \mathrm{) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< l_1\mathrm{: \, if \; (} e' \mathrm{) \; goto} \; l_2, \, \sigma' \right>}$

$\frac{}
{\left<  l_1\mathrm{: \, if \; (0) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_1+1), \, \sigma \right>}$

$\frac{z \ne 0}
{\left< l_1\mathrm{: \, if \; (} z \mathrm{) \; goto} \; l_2, \, \sigma \right>
\rightarrow
\left< P(l_2), \, \sigma \right>}$

$\frac{}
{\left< end, \sigma \right> \rightarrow \mathrm{program \; terminates}}$

$\frac{z_1 > z_2}
{\left< z_1 \mathrm{>} z_2, \, \sigma \right>
\rightarrow
\left< 1, \, \sigma \right>}$

$\frac{\left< e_1, \, \sigma \right> \rightarrow \left< e_1', \, \sigma' \right>}
{\left< e_1 > e_2, \, \sigma \right> \rightarrow \left< e_1' > e_2, \, \sigma' \right>}$

$\frac{\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma' \right>}
{\left< z > e, \, \sigma \right> \rightarrow \left< z > e', \, \sigma' \right>}$

Other comparison operators are analogous.

$\frac{x \in Dom(\sigma)}
{\left< x, \, \sigma \right> \rightarrow \left< \sigma(x), \, \sigma \right>}$

$\frac{x \in Dom(\sigma) \; \;
\left< e, \, \sigma \right> \rightarrow \left< e', \, \sigma'\right>}
{\left<x[e], \, \sigma \right> \rightarrow \left< x[e'], \, \sigma' \right>}$

$\frac{x[z] \in Dom(\sigma)}
{\left<x[z], \, \sigma \right> \rightarrow \left< \sigma(x[z]), \, \sigma \right>}$

$\frac{len(x) \in Dom(\sigma)}
{\left< len(x), \, \sigma \right> \rightarrow \left< \sigma(len(x)), \, \sigma \right>}$

}

\end{document}
